\documentclass[envcountsame,english]{llncs}
\usepackage{babel,url,color}
\usepackage{latexsym,amssymb,amsmath,ifthen,alltt,array,enumerate}
\usepackage{tikz}
\usepackage{float}

\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\mi}[1]{\mathit{#1}}
\newcommand{\GG}{\mathcal{G}}
\newcommand{\seq}[2][n]{{#2_1},\dots,{#2_{#1}}}

\def\test#1#2#3{\setbox0=\hbox{$\vphantom{#1}^{#2}_{#3}$}%
                \dimen0=\wd0%
                \setbox1=\hbox{$\scriptstyle #2$}%
                \advance\dimen0-\wd1%
                \setbox1=\hbox{\hskip\dimen0\copy1}%
                \dimen0=\wd0%
                \setbox2=\hbox{$\scriptstyle #3$}%
                \advance\dimen0-\wd2%
                \setbox2=\hbox{\hskip\dimen0\copy2}%
                {\vphantom{#1}^{\box1}_{\box2}}{#1}
}


\newcommand{\SAT}{3-SAT }
\newcommand{\NP}{NP}
\newcommand{\PSPACE}{PSPACE}
\newcommand{\QBF}{\texttt{QBF }}
\newcommand{\tod}{\overset{d}{\to}}
\newcommand{\toa}{\overset{a}{\to}}

% for editing
\newcommand{\comment}[1]{\begin{center}\color{red}\tt #1 \end{center}}
\newcommand{\FB}[1]{{\color{red}#1}}
\newcommand{\DK}[1]{{\color{blue}#1}}

\newcommand{\dd}{{\langle d \rangle}}

\tikzstyle{mystyle}=[semithick]
\tikzstyle{ledge}=[font=\scriptsize]
\tikzstyle{final}=[circle,draw,minimum size=0.1cm,inner sep=1.7pt]

\begin{document}

\bibliographystyle{lncs}
\pagestyle{plain}


\title{The Multi-Agent Sabotage Game}

\mainmatter

\author{Fran\c{c}ois Bonnet \and Xavier D\'efago \and Dominik Klein}

\institute{School of Information Science\\
Japan Advanced Institute of Science and Technology\\
  Nomi, Japan}

\maketitle

\begin{abstract}
We consider an abstract scenario of malicious agents invading a network, 
modeled as a game. The globally controlled agents move 
alternatingly with a defender: in each turn, 
each agent moves alongside an edge on a directed acyclic graph (DAG), 
trying to reach a single, designated goal vertex, after which 
the defender is allowed 
to remove one edge from the DAG. We show that the 
problem of deciding whether there exists a strategy for the defender to 
disconnect the goal before one of the agents reaches it, is PSPACE-complete 
in general, and that it shifts to NP-complete if we assume an infinite supply
of agents. Moreover, we show that if we fix a constant number of agents and
consider only trees, the problem can be decided in 
polynomial time in the size of the tree.
Our work extends results on the Sabotage Game and the Firefighting problem,
introduced respectively in 2005 by van Benthem and in 1995 
by Hartnell.
\end{abstract}

\section{Introduction}
%DK changed next line
Measuring the reliability of a network under fault is an important task in several
domains, 
especially in the context of analyzing reactive systems.
A natural modeling of such scenarios is the use of two-player games, where one 
player tries to establish a connection between nodes, whereas the other player
tries to destroy this connection. Very famous is the 
Shannon-Switching Game~\cite{LEH64}, but a large number of other graph
based games exist~\cite{DEM01}.
Recently, the ability of restoring destroyed links~\cite{RT07}, and 
other, more general reachability objectives, have been considered~\cite{GRT10}.

In 2005, van Benthem proposed the Sabotage Game~\cite{Ben05}, where 
the first player is subject to local movements in the graph, whereas the
other player is allowed to destroy links anywhere in the graph. 
More specifically, in this game played on graphs with
multi-edges, an agent (a ``Runner'' in their terminology) 
starts at a vertex trying to reach a designated goal, and
in each turn, the agent selects an outgoing edge from his current position 
and moves along that edge. The defender (the ``Blocker'') is then allowed 
to select one edge arbitrarily in the graph and reduce its 
multiplicity by one. The agent wins
if she has a strategy to reach the goal, despite any possible deletions by 
the defender, and she looses otherwise. Adding such kind of dynamics makes
the analysis much more difficult, and often shifts the complexity to 
non-tractable complexity classes, one most notable exception being the 
Shannon-Switching Game. For
Sabotage Games, L\"oding and Rohde~\cite{LR03b} showed that the introduction of 
multi-edges shifts the problem to PSPACE-complete, whereas the game played
over a single-edge graph is decidable in linear time.

Our contribution extends their complexity result. We consider the case 
where the underlying
structure is quite restricted --- a cycle-free digraph ---, but
allow more than one agent to move through the graph.
In each turn, each of the agents, for which we assume some global control,
moves alongside an outgoing edge from its current position. Then the
defender is allowed to remove one edge from the graph and the next turn starts.
The agents win, if,
after several turns, at least one of them reaches the designated goal. We show that 
adding this kind of distributivity leads to a similar shift in complexity, 
even though the underlying, dynamically
changing structure is simpler. More specifically, our contribution includes 
the following four results:

\begin{itemize} %DK slight changes to avoid starting too many items with "We show"
% and shorten to gain space for a description of the firefigther-problem
\item deciding whether the defender can always prevent 
$n$ agents from reaching the goal is PSPACE-complete, except for $n=1$.
\item playing against infinitely many agents shifts the problem
to NP-complete. %DK algorithm -> attractor construction.
\item for games over trees and a fixed number of agents, we give an 
attractor-construction that computes whether the agents can be 
prevented from reaching the goal in time polynomial in the size of the tree.
\item games over trees however remain NP-hard for infinitely
many agents.
\end{itemize}

%DK added a short description of firefigher problem...
To establish the last, we use 
a very straight-forward reduction from 3-FL-FIRE~\cite{KG10}, 
a variant of the Firefighter-problem on trees with reachability
conditions. 
In the Firefigher-problem~\cite{H95}, a fire starts at a desginated vertex. In each step,
the Firefighter chooses a non-burning vertex to protect, which 
remains protected afterwards. Then the fire spreads to all
adjacent vertices. This continues, until the fire cannot spread anymore. The
Firefigher-problem asks to maximize the number of saved vertices.

The fourth result of course subumes the second, since we regard 
a tree as a special kind of DAG.
We would like to stress however, that establishing NP-hardness 
of 3-FL-FIRE itself is quite involved, reusing a central 
result from~\cite{FKMR07}
and several layers of reductions, whereas our proof of NP-hardness 
of playing against infinitely many agents 
on DAGs is a direct reduction 
from SAT, based on the completely different machinery 
we develop to establish the result of PSPACE-hardness, 
albeit requiring full DAGs.

%DK: slightly changed
This paper is structured as follows: In Section~\ref{sec:definitions} we 
define the multi-agent sabotage game and the decision problem $n$-AGENT BLOCKING, 
for which we show PSPACE-completeness in Section~\ref{sec:PSPACE-completeness}.
NP-completeness of INFTY-AGENT BLOCKING, where the number of agents is infinite,
is established in  Section~\ref{sec:np-hard}. In Section~\ref{sec:tree} we 
consider games over trees and show that then $n$-AGENT BLOCKING 
can be computed in time polynomial in the size of the tree for a constant number
of agents, but remains NP-hard when considering infinitely many.
Finally we conclude our presentation in Section~\ref{sec:Conclusion} 
and mention potential future work.


\section{Multi-Agent Sabotage Game}
\label{sec:definitions}

%DK outcommented first sentence
%We give a formalization of the multi-agent blocking problem.
A multi-agent game is played on a game-arena 
$\GG=(G,s,f)$ where $G=(V,E_{\text{in}})$ is a directed acyclic graph (DAG)\footnote{
All results presented here hold for unrestricted digraphs as well.},
$s$ is the \emph{initial} node, and $f$ is the \emph{goal} node. %DK added \emph{}

For a game with $n$ agents on a graph $G=(V,E_{\text{in}})$, a \emph{configuration} is a 
tuple $(E,A)$, where $E$ is a subset of $E_{\text{in}}$ and $A$ is a multiset 
of vertices $V$ with $|A|=n$, denoting the current positions of agents.
%Note that the set of vertices $V$ does not need to be included in configurations since it does not
%change during the game. 
The game is played by alternating moves of the agents and the defender. %DK the...
Let $(E,A)$ and $(E',A')$ be two configurations:
\begin{itemize}
\item A \emph{move of the agents} $(E,A) \toa (E',A')$ requires $E = E'$ 
and the existence of a multiset $S$ of vertices from $V$ and
a multiset $M$ of edges from $E$ such that
$A = S \uplus \{ s \mid (s,t) \in M \}$ and 
$A' = S \uplus \{ t \mid (s,t) \in M \}$, i.e. the agents in $S$ remain at
their position, whereas the rest moves alongside edges in $M$.
\item A \emph{move of the defender} $(E,A) \tod (E',A')$ requires
$A = A'$ and $E' = E \setminus \{e\}$ where $e \in E$, we say defender \emph{deletes} $e$.
\end{itemize} 

\noindent Let $\GG=(G,s,f)$ be a game-arena with $G=(V,E_{\text{in}})$ and $|E_{\text{in}}|=k$.
Assuming $n$ agents, the \emph{initial configuration} of $\GG$ is $c_{\text{in}}=(E_{\text{in}},A_{\text{in}})$ where 
$A_{\text{in}} = \{ \overbrace{s, \ldots, s}^{\text{$n$ times}} \}$.
For a configuration $c=(E,A)$, property $\text{win}(c)$ holds if
$f \not \in A$, i.e. no agent has reached the goal node. %DK removed paragraph
The defender \emph{wins} in $\GG$ against $n$ agents, if 
\[
\forall c_1 \exists c'_1 \forall \ldots \forall c_{k-1} \exists c'_{k-1} \forall c_{k}\,\
c_{\text{in}} \toa c_1 \tod \ldots \toa c_{k-1} \tod c'_{k-1} \toa c_k \Rightarrow \text{win}(c_k)
\]
\noindent where $c_{\text{in}}$ denotes the initial configuration of $\GG$.

\begin{quote}
\emph{$n$-AGENT BLOCKING} is the following decision problem: \\
\textsf{Input:} A game-arena $\GG$ \\
\textsf{Question:} Does the defender win in $\GG$ against $n$ agents?
\end{quote}

\subsection{PSPACE-completeness of blocking $n$ agents}\label{sec:PSPACE-completeness}

We first consider the case where there is only one agent. 
This corresponds to a special case of the Sabotage Game~\cite{LR03b}, 
where the multiplicity of each edge is one. We have:

\begin{lemma}[\cite{LR03b}]\label{lem:neq1}
$1$-AGENT BLOCKING is decidable in linear time.%dk:changed name
\end{lemma}
%%FB: I modify the proof to take in consideration the fact that agents play first.
%%FB: I added some formalization and (I hope) simplification.
%DK: I shortened the proof slightly :-)
\begin{proof}
The agent wins iff $s=f$ or $(s,f)\in E_{\text{in}}$. If not, the defender has the following winning strategy: If the agent is at vertex $v$ and there is an edge $(v,f) \in E$, the defender
deletes $(v,f)$. Otherwise the defender deletes an edge arbitrarily.
\end{proof}

If we consider more than one agent, the complexity changes:

\begin{theorem}\label{thm:pspace-complete}%dk:changed name
$n$-AGENT BLOCKING is PSPACE-complete for all $n \geq 2$.
\end{theorem}

To prove Theorem~\ref{thm:pspace-complete}, we need to show 
membership in PSPACE, 
and PSPACE-hardness. The first can be shown by a 
depth-first game-tree construction, here we focus 
only on the latter. For it, we give a reduction from 
the PSPACE-complete problem of Quantified Boolean 
Formula (QBF)~\cite{ST73}. 

Let
$\psi = \forall X_1 \exists X_2 \ldots Q X_{m-1} Q X_m \varphi$
be an instance of QBF, where $\varphi$ is a quantifier free formula 
over the $m$ Boolean variables $X_1, \ldots X_m$ in conjunctive normal form
with $p$ clauses,
and $Q$ is $\forall$ for $m$ odd and $\exists$ for $m$ even.

Note that w.l.o.g. we can assume that each clause contains 
exactly three distinct literals. 
Unless stated otherwise, we use indices in the following 
way: $1 \leq i \leq m$ ranges
over the $m$ variables, $1 \leq j \leq p$ over clauses and
$1 \leq k \leq 3$ over literals of clauses.
For a given $\psi$ and a given $n$,
we will construct a (parametrized) game-arena 
$\GG^{n}_{\psi}$ with $n$ agents placed at the starting node.


\begin{lemma}\label{lem:g_qbf_psi}
Let $\psi$ be an instance of QBF and $n \in \mathbb{N}$ with 
$n \geq 2$. The defender wins on $\GG^{n}_{\psi}$ 
iff $\psi$ has a satisfying assignment.
\end{lemma}

Lemma~\ref{lem:g_qbf_psi} and polynomial size of the game-arena
in the size of $\psi$ and $n$, proves 
Theorem~\ref{thm:pspace-complete}. The rest of this section 
shows how to construct $\GG^{n}_{\psi}$.
%First note the two following simple facts: (i) As soon as the
%agents reach a configuration $c$ where $\text{win}(c)$ holds,
%the game is essentially over. Indeed the agents located at the goal
%node just remain there until all edges have been deleted.
%(ii) If there are $n$ agents and $n-1$ are
%``stuck'', i.e. have no outgoing edge to move on, the last
%agent can be stopped with the strategy described in
%Lemma~\ref{lem:neq1}. In the reduction we will make use of 
%these facts and the interaction of precisely two agents 
%that have to behave in a certain way in order
%to prevent one agent from being stuck.

We adapt the idea used for the reduction of the
Sabotage Game~\cite{LR03b} to our setting. Naturally,
our construction is different since we are in 
a different setting,
but the following underlying principle is 
employed: we construct
a game-arena, where first, the agents and the defender 
make an assignment of the variables \emph{in the graph} 
by their movements. 
If this assignment satisfies the formula, then the defender
wins in a later part of the graph, and she looses otherwise. In
particular we use the following substructures:


%DK I changed the description of universal gadget
%DK removed the ... in the graph ... - part, since this is defined only later
\begin{itemize}
 \item The \emph{filtering-gadget} is used as a barrier such that when $n$ agents enter it, precisely two agents are able to pass it.
 \item A \emph{universal-gadget} corresponds to a universally quantified variable. The 
 movements of the agents determine whether the corresponding variable is set 
 either to \textsc{true} or \textsc{false}.
\item An \emph{existential-gadget} corresponds to one existentially quantified variable. Depending on his deletions, the defender may assign \textsc{true} or \textsc{false} to the variable.
 \item The \emph{verification-gadget}: Here the agents can choose a clause --- with the intention of showing that the defender's assignment of variables is not a satisfying one ---, and after the movements lead to that clause, by subsequent deletions, the defender can choose one literal in the clause, with the intention of showing that for any clause there is at least one literal that satisfies it.
\end{itemize}


%DK outcommented one line (\psi is already defined above)
%Let $\psi = \forall X_1 \exists X_2 \ldots Q X_{m-1} Q X_m \varphi$ 
%and assume $n$ agents. 
%removed brackets
The gadgets will be connected in the following way: 
the start of the game-arena $\GG^n_{\psi}$ is the filtering-gadget; the starting node 
$s$ of the game-arena is the node $s_0$ of this gadget.
The exit node $s_1$ of the filtering gadget corresponds to the entry of the 
universal-gadget for $X_1$, whose exit node $s_2$ corresponds to the entry
of the existential-gadget for $X_2$ etc., until the last variable gadget for $X_m$,
whose exit node $s_{m+1}$ is connected to the verification-gadget.
We define the correspondence of an assignment of the variables of $\psi$ and 
movements and deletions in $\GG^n_{\psi}$. Here nodes $x_i$ and $\neg x_i$ denote two 
particular nodes of the graph:

%DK changed E_in to E, and added notion of configuration, otherwise definition makes not
% much sense.
%DK we should change the remaining lemmata accordingly. 
\begin{definition}
Let $\GG^n_{\psi} = (G,s,f)$ be the game-arena for a given instance $\psi$ of QBF, and $(E,A)$ a configuration. Variable
$X_i$ is assigned \emph{in} $\GG^n_{\psi}$ to
\begin{align*}
&\text{\textsc{false}, when $(x_i,f) \in E$ and $\textsf{outdeg}(\neg x_i) = 0$}  \\
&\text{\textsc{true}, when $(\neg x_i,f) \in E$ and $\textsf{outdeg}(x_i) = 0$}  
\end{align*}
We write $\GG^n_{\psi}(X_i) = \textsc{true}$ resp. $\GG^n_{\psi}(X_i) = \textsc{false}$,
and we write $\alpha(\GG^n_{\psi})$ to denote 
the assignment of the variables of $\psi$ where $X_i = \textsc{true}$ when 
$\GG^n_{\psi}(X_i) = \textsc{true}$ and $X_i = \textsc{false}$ when $\GG_{\psi}^n(X_i) = \textsc{false}$.
\end{definition}

In the following figures we often draw multiple goal nodes. This is only for the ease of illustration, and all goal nodes of all occurring gadgets can be actually merged into a single goal node.

\subsection*{The filtering-gadget}

The initial state of the filtering-gadget for $n$ agents, before any edge-removal by the defender, is shown in Figure~\ref{fig:filtering-gadget_init}, and the agents are about to move. The filtering-gadget has the following property:

%DK changed Lemma
\begin{lemma}\label{lem:filtering}
Let $G$ be a graph containing a filtering gadget. The defender wins in $(G,s_0,f)$ against $n$ agents iff the defender wins in $(G,s_1,f)$ against two agents.
\end{lemma}

Assume one agent moves to each $a_{i,1}$ for $1 \leq i \leq n-2$. Moving more than one agent to one of the $a_{i,1}$ is not optimal, since from each $a_{i,1}$ there is only a single path to the goal. The remaining two agents move to $b_1$. The defender has to remove the edge $(a_{1,1},f)$, the agents proceed to $b_{2}$ and $a_{i,2}$ for $2 \leq i \leq n-2$, the defender removes the edge $(a_{2,2},f)$, and so on, until the agents reach $a_{n-2,n-2}$ and $b_{n-2}$. The defender removes the edge $(a_{n-2,n-2},f)$, and two agents reach $s_1$ from $b_{n-2}$. Any other movements of players lead to a loss for them.

%DK s -> s_0
\begin{figure}[t]%
  \centering 
 \parbox{0.45\textwidth}{%
  % The initial filtering gadget
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
    \tikzstyle{every to}=[->] %make all edges directed

    \node[]  								(a)		at (0,0)  {$s_0$};    
    
    \node[]									(a21)		[below of=a] 	{$a_{2,1}$};
	\node[]									(a11)		[left of=a21] 	{$a_{1,1}$};
	\node[]									(b1)		[left of=a11]	{$b_1$};
	
	\node[node distance=2cm]				(am1)		[right of=a21] 	{$a_{n-2,1}$};
    
    \node[]									(b2)		[below of=b1]	{$b_2$};
    \node[]									(a22)		[below of=a21]	{$a_{2,2}$};
    
    
    \node[node distance=2cm, style=final]	(f)	 		[below of=a22]	{$\bullet$}; 
    \node[node distance=3cm]				(bm)		[below of=b1]	{$b_{n-2}$};
    \node[]									(b)			[below of=bm]	{$s_1$};
    
    \node[node distance=3cm]				(amm)		[below of=am1]	{$a_{n-2,n-2}$};
    
 	\draw[style=dotted] (a21) 	to[-] node[auto] {} (am1);
	\draw[style=dotted] (b2) 	to[-] node[auto] {} (bm);
	\draw[style=dotted] (am1) 	to[-] node[auto] {} (amm);
	
	\draw[]						(a)		to node[auto]	{}	(b1);
	\draw[]						(b1)	to node[auto]	{}	(b2);
	\draw[]						(bm)	to node[auto]	{}	(b);	
	\draw[]						(a)		to node[auto]	{}	(a11);
	\draw[]						(a21)	to node[auto]	{}	(a22);				
	\draw[]						(a)		to node[auto]	{}	(a21);
	\draw[]						(a)		to node[auto]	{}	(am1);
	
	\draw[bend right = 20]		(a11)	to node[auto]	{}	(f);
	\draw[]						(a22)	to node[auto]	{}	(f);
 	\draw[bend left = 20]		(amm)	to node[auto]	{}	(f);
  
    
  \end{tikzpicture}
  \caption{The filtering-gadget}
  \label{fig:filtering-gadget_init}  } %
  \parbox{0.45\textwidth}{%
  % The universal gadget
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(a)		at (0,0)			{$s_i$};

	\node[]								(c1)		[below left of=a] 	{$c_1$};
	\node[]								(c2)		[below right of=a] 	{$c_2$};	
	\node[]								(d1)		[below left of=c1] 	{$d_1$};	
	\node[]								(d2)		[below right of=c2] {$d_2$};

	\node[node distance=2cm]			(e1)		[below left of=d1]	{$e_1$};
	\node[node distance=2cm]			(e2)		[below right of=d1]	{$e_2$};
	
	\node[]								(g1)		[right of=e1]		{$x_i$};
	\node[]								(g2)		[left of=e2]		{$\neg x_i$};

	\node[node distance=2cm]			(h1)		[below of = e2]		{$h_1$};
	\node[]								(i1)		[below of = h1]		{$i_1$};
    \node[style=final]					(f3) 		[right of=i1]		{$\bullet$}; 
	\node[]								(b)			[below of = f3]		{$s_{i+1}$};

    \node[node distance=2.4cm,style=final](f0) 		[right of=a]		{$\bullet$};
    \node[node distance=2.4cm,style=final](f1) 		[below of=d1]		{$\bullet$}; 
    \node[node distance=1.7cm,style=final](f2) 		[right of=c2]		{$\bullet$}; 
    \node[style=final]					(f3) 		[right of=d2]		{$\bullet$}; 
    \node[style=final]					(f4) 		[right of=i1]		{$\bullet$}; 

	\node[node distance=2cm]			(er)		[below right of=d2]	{$e_r$};
	\node[]								(hl)		[left of=er]		{$h_l$};
	\node[]								(hr)		[below of=er]		{$h_r$};
    \node[style=final]					(f5) 		[left of=hr]		{$\bullet$}; 
	\node[]								(i2)		[below of=f5]		{$i_2$}; 
	
	\node[node distance=1.4cm]			(from_veri1)[left of=d1]		{\tiny{ver. gadget}};
	\node[node distance=1.5cm]			(from_veri2)[below of=e1]		{\tiny{ver. gadget}};
 
	\draw[]								(a)			to node[auto]	{}	(c1); 		
	\draw[]								(a)			to node[auto]	{}	(c2); 		
	\draw[]								(c1)		to node[auto]	{}	(d1); 		
	\draw[]								(c2)		to node[auto]	{}	(d2); 			 	
	\draw[]								(d1)		to node[auto]	{}	(e1); 			 	
	\draw[]								(d1)		to node[auto]	{}	(e2); 			 	
	\draw[]								(e1)		to node[auto]	{}	(g1); 			 	
	\draw[]								(e2)		to node[auto]	{}	(g2); 			 	
	\draw[]								(g1)		to node[auto]	{}	(f1); 			 	
	\draw[]								(g2)		to node[auto]	{}	(f1); 			 	
	\draw[]								(e2)		to node[auto]	{}	(h1); 			 	
	\draw[bend left=-30]				(e1)		to node[auto]	{}	(h1); 			 	
	\draw[]								(h1)		to node[auto]	{}	(i1); 			 	
 	
	\draw[]								(i1)		to node[auto]	{}	(b); 			 	
	\draw[]								(i1)		to node[auto]	{}	(f4); 			 	

	\draw[]								(d2)		to node[auto]	{}	(er); 			 	
	\draw[]								(er)		to node[auto]	{}	(hl); 			 	
	\draw[]								(er)		to node[auto]	{}	(hr); 			 	
	\draw[]								(hl)		to node[auto]	{}	(f5); 			 	
	\draw[]								(hr)		to node[auto]	{}	(f5); 			 	
	\draw[]								(hr)		to node[auto]	{}	(i2); 			 	
	\draw[bend left=-40]				(hl)		to node[auto]	{}	(i2); 			 	
	\draw[bend right=-20]				(i2)		to node[auto]	{}	(b); 			 	
	\draw[]								(a)		to node[auto]	{}	(f0);
	\draw[]								(c2)		to node[auto]	{}	(f2); 			 	
	\draw[]								(d2)		to node[auto]	{}	(f3); 

	\draw[bend left=20,style=ledge,dotted]	(from_veri1) to node[auto] {} (g2);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (g1); 	
 	
  \end{tikzpicture}
  \caption{The initial \emph{universal} gadget for variable $X_i$.}
  \label{fig:universal-gadget}
}

\end{figure}

\subsection*{The universal-gadget}
%DK an universal gadget -> a universal gadget
A universal-gadget is shown in Figure~\ref{fig:universal-gadget}. 
One universal-gadget corresponds to one universally quantified variable. 
The universal-gadget corresponding to variable $X_i$ is connected
with the verification-gadget in the following way:
Let $L_{jk}$ be a literal of $\psi$. Then
$(l_{jk},x_i) \in E_{\text{in}}$ iff $L_{jk} = X_i$, and 
$(l_{jk},\neg x_i) \in E_{\text{in}}$ iff $L_{jk} = \neg X_i$. Here
$l_{jk}$ is a node in the verification-gadget.
In a universal-gadget, the agents may choose an assignment:

\begin{lemma}\label{lem:universal}
Let $X_i$ be the variable of a universal-gadget of $\GG^n_{\psi}$, and $(E,\{s_i, s_i\})$ be a configuration, where the edges of the gadget $E_u \subseteq E$ are intact. 
Let both player play optimally.
Then a traversal of the universal-gadget leads to a configuration $(E',\{s_{i+1}, s_{i+1}\})$ 
where $E' \setminus E_u = E \setminus E_u$ and, \emph{depending on the movements of the agents},  either 
$\GG^n_{\psi}(X_i) = \textsc{true}$ or $\GG^n_{\psi}(X_i) = \textsc{false}$.
\end{lemma}

Assume that two agents arrive at node $s_i$ (from either the filtering-gadget or a previous existential-gadget), then defender has to remove the edge $(s_i,f)$ otherwise he looses the game. For agents, moving both to $c_1$ leads to loss, as does moving both to $c_2$ after subsequent deletions of $(c_2,f)$, $(d_2,f)$, $(e_r,h_l)$, $(h_r,f)$, and $(i_2,b)$. Thus the agents split and move to $c_1$ and $c_2$, and after deleting $(c_2,f)$ arrive at $d_1$ and $d_2$, and $(d_2,f)$ is deleted. Now the left agent may decide to either move to $e_1$ (which will result in assigning $X_i$ to \textsc{false} in $\GG_{\psi}^n$) or to $e_2$ (which will result in  assigning $X_i$ to \textsc{true}), whereas the agent on $d_2$ moves to $e_r$. Assume the first. The defender has to delete either $(e_1,x_i)$ or $(x_i,f)$, otherwise he looses by moves of the agents to both $x_i$ and to either $h_l$ or $h_r$. The defender will remove $(x_i,f)$, as this blocks also all incoming edges from the verification gadget. After several subsequent moves and deletions, both agents arrive at $s_{i+1}$. The case when the left agent moves to $e_2$ is analogous, and
other movements of the players lead to their loss.

\subsection*{The existential-gadget}

\begin{figure}[]%
  \centering

  % The existential gadget
  \begin{tikzpicture}[scale=0.2,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

    \node[]								(b)	at (0,0)		{$s_i$};    
   
    \node[node distance=2.08cm, style=final](f) 	[below of=b]		{$\bullet$};    
    \node[node distance=1.5cm]			(bl)		[below left of=b]	{$b_l$};
    \node[node distance = 1.5cm]			(br)		[below right of=b]	{$b_r$};   

    \node[]								(cl)		[below of=bl]		{$c_l$};   
    \node[]								(cr)		[below of=br]		{$c_r$};   
    \node[]								(el)		[below of=cl]		{$x_i$};   
    \node[]								(er)		[below of=cr]		{$\neg x_i$};   
    \node[]								(dl)		[left of=el]		{$d_l$};   
    \node[]								(dr)		[right of=er]		{$d_r$};   
    \node[node distance=2cm]			(g)			[below of=f]		{$g$};
    \node[]								(o)			[below of=g]		{$s_{i+1}$};
    
    \node[node distance=2cm]			(h)			[left of=cl]		{$h$};    
    \node[]								(i)			[below of=h]		{$i$};
    \node[]								(j)			[left of=i]			{$j$};
    \node[]								(k)			[below of=i]		{$k$};
    \node[style=final]					(f2)		[below of=j]		{$\bullet$};

    \node[node distance=3cm]		(from_veri1)[above left of=i]	{\tiny{ver. gadget}};
    \node[node distance=1.5cm]		(from_veri2)[above right of=dr]	{\tiny{ver. gadget}};
 
	\draw[]							(b)		to node[auto]	{}	(bl); 
	\draw[]							(b)		to node[auto]	{}	(br);     
	\draw[]							(bl)	to node[auto]	{}	(cl); 	
	\draw[]							(br)	to node[auto]	{}	(cr); 		
	\draw[]							(cl)	to node[auto]	{}	(dl); 		
	\draw[]							(cr)	to node[auto]	{}	(dr); 		
	\draw[]							(dl)	to node[auto]	{}	(g); 	
	\draw[]							(dr)	to node[auto]	{}	(g); 	
	\draw[]							(dl)	to node[auto]	{}	(el); 	
	\draw[]							(dr)	to node[auto]	{}	(er); 	
	\draw[]							(g)		to node[auto]	{}	(o); 		
	
	\draw[]							(bl)	to node[auto]	{}	(h); 		
	\draw[]							(h)		to node[auto]	{}	(i); 	
	\draw[]							(i)		to node[auto]	{}	(k); 	
	\draw[]							(i)		to node[auto]	{}	(j); 	
	\draw[]							(k)		to node[auto]	{}	(o); 	
%	\draw[out=-130, in=-140,looseness=1.2]	(j)		to node[auto]	{}	(o); 			
	\draw[out=-130, in = -180]	(j)		to node[auto]	{}	(o); 			
	
	
	\draw[]							(cl)	to node[auto]	{}	(f); 	
	\draw[]							(bl)	to node[auto]	{}	(f); 	
	\draw[]							(cr)	to node[auto]	{}	(f); 	
	\draw[]							(br)	to node[auto]	{}	(f); 	
	\draw[]							(el)	to node[auto]	{}	(f); 	
	\draw[]							(er)	to node[auto]	{}	(f); 	
	\draw[]							(j)		to node[auto]	{}	(f2); 	
	\draw[]							(k)		to node[auto]	{}	(f2); 	

	\draw[bend left=30,style=ledge,dotted]	(from_veri1) to node[auto] {} (el);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (er);
	\draw[looseness=2.5]		(br)	to node[auto]	{}	(h);	
  \end{tikzpicture}
  \caption{The initial \emph{existential} gadget for variable $X_i$.}
  \label{fig:existential-gadget}
\end{figure}

An existential-gadget is shown in Figure~\ref{fig:existential-gadget}. 
One existential-gadget corresponds to one existantially quantified variable. 
The existential-gadget corresponding to variable $X_i$ is connected
with the verification-gadget in the following way:
for $L_{jk}$ denoting the $k$-th literal of the $j$-th clause $C_j$ of $\psi$, we have
$(l_{jk},x_i) \in E$ iff $L_{jk} = X_i$, and 
$(l_{jk},\neg x_i) \in E$ iff $L_{jk} = \neg X_i$, where
$l_{jk}$ is a node in the verification-gadget.
The key point here is that the defender can choose an assignment:

\begin{lemma}\label{lem:existential}
Let $X_i$ be the variable of an existential-gadget of $\GG^n_{\psi}$, and $(E,\{s_i, s_i\})$ be a configuration, where the edges of the gadget $E_e \subseteq E$ are the intact.
Let both player play optimally.
Then a traversal of the existential-gadget leads to a configuration $(E',\{s_{i+1}, s_{i+1}\})$ 
where $E' \setminus E_e = E \setminus E_e$ and, \emph{depending on the deletions of the defender}, either
$\GG^n_{\psi}(X_i) = \textsc{true}$ or $\GG^n_{\psi}(X_i) = \textsc{false}$.
\end{lemma}

Assume that two agents arrive at node $s_i$ (from a previous universal-gadget), 
the choice of the defender is done by deleting either $(s_i,b_l)$ or $(s_i,b_r)$ in the first step,
the former assigns $X_i$ to \textsc{true} in $\GG^n_{\psi}$, the latter to 
\textsc{false}. Consider the following traversals:
If neither $(s_i,b_l)$ or $(s_i,b_r)$ has been deleted, the 
agents win by moving one agent to $b_l$ and one to $b_r$ and 
then one of them to the goal, or, if either $(b_l,f)$ or 
$(b_r,f)$ has been deleted in the first step, 
by continuing to $(c_l,f)$ and $(c_r,f)$ and then moving 
one of the agents to the goal.

For now assume that the defender deletes $(s_i,b_r)$. 
Thus the agents move both to $b_l$, and defender removes 
$(b_l,f)$. Moving both agents to $h$ leads to loss by 
removing $(h,i)$, and moving both to $c_l$ also 
leads to loss by deleting $(c_l,f)$, then $(d_l,x_i)$ 
and finally $(g,s_{i+1})$. Thus the agents have to split 
and one moves to $h$ and one to $c_l$. Defender 
deletes $(c_l,f)$ and the agents move to $i$ and $d_l$.

If neither $(d_l,x_i)$ or $(x_i,f)$ is deleted, the 
agents win by moving both to $x_i$ and to either $j$ 
or $k$. It will be later seen that it is optimal now for the 
defender to remove the edge $(x_i,f)$, thereby disconnecting 
any link back from the verification gadget. Afterwards the 
agent at $d_l$ moves in two steps via $g$ to $s_{i+1}$, and 
the other one either via $k$ --- defender 
removing $(k,f)$ --- or via $j$ --- defender 
removing $(j,f)$ --- to $s_{i+1}$. 

    
  
\begin{figure}[]%
  \centering  
  % The verification gadget
  \begin{tikzpicture}[scale=0.3,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(a)			at (0,0) {$s_{m+1}$};
 	\node[node distance=0.8cm]			(fake2)		[below of=a]		{};
	\node[node distance=2cm]			(dl)		[left of=fake2]		{$d_l$};
	\node[node distance=2cm]			(dr)		[right of=fake2]	{$d_r$};
	\node[]								(el)		[below of=dl]		{$e_l$};
	\node[]								(er)		[below of=dr]		{$e_r$};
	\node[]								(fr)		[below of=er]		{$f_r$};
	\node[]								(fl)		[below of=el]		{$f_l$};
    \node[style=final, node distance = 3cm]			(f0) 		[right of=a]		{$\bullet$}; 
    \node[style=final]					(f1) 		[right of=dr]		{$\bullet$}; 
    \node[style=final]					(f2) 		[left of=el]		{$\bullet$}; 
    \node[style=final]					(f3) 		[right of=fr]		{$\bullet$}; 
    
    \node[]								(fake_c)	[below of=fl]		{$\cdots \cdots$};
    \node[]								(fake_c2)	[left of=fake_c]	{$l_{21}$};
    \node[]								(fake_ck)	[right of=fake_c]	{$l_{(p-1)1}$};
    \node[node distance = 1.5cm]		(c1)		[left of=fake_c	]	{$l_{11}$};    
    \node[node distance = 2cm]			(ck)		[right of=fake_c]	{$l_{p1}$};
    
    \node[]								(fake_right)[below of=fr]		{};    
    \node[]								(g)			[right of=fake_right]{$l_{r1}$};

	\node[]								(fake_mid1)	[below of = c1]		{};    
    \node[]								(fake_l11)	[left of=fake_mid1] {};
    \node[]								(h1)		[right of=fake_mid1]{$g_1$};
    
    \node[]								(fake_midk)	[below of=ck]		{};
    \node[]								(fake_lk1)	[left of=fake_midk]	{};
    \node[]								(hk)		[right of=fake_midk]{$g_p$};
    \node[]								(hl)		[below of=g]		{$g_l$};
    \node[]								(hr)		[right of=g]		{$g_r$};
    \node[style=final]					(f4) 		[right of=hl]		{$\bullet$}; 

	\node[]								(i1)		[below of=h1]		{$l_{12}$};
	\node[node distance=1.5cm]			(mid_dots)	[right of=i1]	{$\cdots \cdots$};
	\node[]								(ik)		[below of=hk]		{$l_{k2}$};
	\node[]								(i)			[below of=hl]		{$l_{r2}$};

	\node[]								(fake_mid2)	[below of=i1]		{};
	\node[]								(fake_l12)	[left of=fake_mid2]	{};
	\node[]								(j1)		[right of=fake_mid2]{$l_{13}$};

	\node[]								(fake_midk2)[below of=ik]		{};
	\node[]								(fake_lk2)	[left of=fake_midk2]{};
	\node[]								(jk)		[right of=fake_midk2]{$l_{k3}$};

	\node[]								(fake_mid3) [below of=j1]		{};
	\node[]								(fake_l13)	[left of=fake_mid3]	{};
	\node[]								(fake_midk3)[below of=jk]		{};
	\node[]								(fake_lk3)	[left of=fake_midk3]{};	
	
	\node[]								(jr)		[right of=i]		{$h_r$};
	\node[]								(jl)		[below of=i]		{$h_l$};
	\node[]								(jf)		[below of=jl]		{$l_{r3}$};
    \node[style=final]					(f5) 		[right of=jl]		{$\bullet$}; 

	\draw[]								(a)			to node[auto]	{}	(dl); 			 	
	\draw[]								(a)			to node[auto]	{}	(dr); 			 	
	\draw[]								(a)		to node[auto]	{}	(f0); 	 	
	\draw[]								(dl)		to node[auto]	{}	(el); 			 	
	\draw[]								(dr)		to node[auto]	{}	(er);
	\draw[]								(dr)		to node[auto]	{}	(f1); 	 			 	
	\draw[]								(er)		to node[auto]	{}	(fr); 			 	
	\draw[]								(el)		to node[auto]	{}	(fl); 	
	\draw[]								(el)		to node[auto]	{}	(f2); 				 	
	\draw[]								(fr)		to node[auto]	{}	(f3); 			 	
	\draw[]								(fl)		to node[auto]	{}	(c1); 				 	
	\draw[]								(fl)		to node[auto]	{}	(ck); 			 	
	\draw[]								(fr)		to node[auto]	{}	(g);	
	\draw[]								(g)			to node[auto]	{}	(hr);	
	\draw[]								(g)			to node[auto]	{}	(hl);
	\draw[]								(hr)		to node[auto]	{}	(f4);
	\draw[]								(hl)		to node[auto]	{}	(f4);
	\draw[]								(hl)		to node[auto]	{}	(i);
	\draw[]								(i)			to node[auto]	{}	(jr);
	\draw[]								(i)			to node[auto]	{}	(jl);	
	\draw[]								(jl)		to node[auto]	{}	(f5);
	\draw[]								(jr)		to node[auto]	{}	(f5);
	\draw[]								(jl)		to node[auto]	{}	(jf);
	\draw[]								(jf)		to node[auto]	{}	(f5);
	
	\draw[style=ledge,dotted]			(c1)		to node[auto]	{\tiny{back}}	(fake_l11);
	\draw[style=ledge,dotted]			(ck)		to node[auto]	{\tiny{back}}	(fake_lk1);
	\draw[]			(c1)		to node[auto]	{}	(h1);
	\draw[]			(ck)		to node[auto]	{}	(hk);	
	\draw[]			(h1)		to node[auto]	{}	(i1);	
	\draw[]			(hk)		to node[auto]	{}	(ik);	
	\draw[]			(i1)		to node[auto]	{}	(j1);	
	\draw[]			(ik)		to node[auto]	{}	(jk);	
	\draw[]			(fl)		to node[auto]	{}	(fake_c2);
	\draw[]			(fl)		to node[auto]	{}	(fake_ck);
	\draw[style=ledge,dotted]			(i1)		to node[auto]	{\tiny{back}}	(fake_l12);	
	\draw[style=ledge,dotted]			(ik)		to node[auto]	{\tiny{back}}	(fake_lk2);	
	\draw[style=ledge,dotted]			(j1)		to node[auto]	{\tiny{back}}	(fake_l13);	
	\draw[style=ledge,dotted]			(jk)		to node[auto]	{\tiny{back}}	(fake_lk3);	

	\draw[out=-5,in=20,looseness=1.1]		(hr)		to node[auto]	{}	(i);	
	\draw[out=-5,in=-10,looseness=1.1]		(jr)		to node[auto]	{}	(jf);	

	
  \end{tikzpicture}
  \caption{The verification-gadget with $p$ clauses.}
  \label{fig:verification-gadget}
\end{figure}

\subsection*{The verification-gadget}

%%FB: Again I changed the indexes, i, j,k to be consistent with everything from the beginning
The verification gadget is depicted in Figure~\ref{fig:verification-gadget}. 
Here a node $l_{jk}$ corresponds to the literal $L_{jk}$ of $\psi$, and has outgoing links to the variable gadgets, as described.
There is a direct correspondence between winning conditions and assignments of literals:

\begin{lemma}\label{lem:veri_literals}
Let $\GG^n_{\psi}$ be the game-arena of $\psi$, and $(E,A)$ a configuration,
where all variables of $\psi$ are assigned \emph{in} $\GG^n_{\psi}$, and
defender is about to move.
\begin{enumerate}
\item Let $A = \{ l_{j1}, l_{r1}\}$. Then defender wins if $\alpha(\GG^n_{\psi}) \models L_{j1}$.
\item Let $A = \{ l_{j2}, l_{r2}\}$. Then defender wins if $\alpha(\GG^n_{\psi}) \models L_{j2}$.
\item Let $A = \{ l_{j3}, h_{l}\}$ or $A = \{ l_{j3}, h_{r}\}$. Then defender wins iff $\alpha(\GG^n_{\psi}) \models L_{j3}$.
\end{enumerate}
\end{lemma}
\begin{proof}
W.l.o.g. let $L_{j1} = X_i$. For the first claim, since $\alpha(\GG^n_{\psi}) \models L_{j1}$, we have $\textsf{outdeg}(x_i) =0$, i.e. $x_i$ is a sink. Thus the defender wins by 
removing $(l_{j1},g_j)$ and applying the strategy of Lemma~\ref{lem:neq1} afterwards.
The second claim follows analogous. For the third claim, w.l.o.g. let $L_{j3} = X_i$. 
When $\alpha(\GG^n_{\psi}) \models L_{j3}$, the defender wins by removing
$(h_{l},f)$ (resp. $(h_{r},f)$) and $(l_{r3},f)$. 
When $\alpha(\GG^n_{\psi}) \not \models L_{j3}$,
after the deletion of the defender, the agents win by either moving 
from $h_l$ ($h_r$) to $f$ or by moving both to $x_i$ and $l_{r3}$, and 
then winning in the next step.
\end{proof}

Using Lemma~\ref{lem:veri_literals}, the following relation between
assignments in $\GG^n_{\psi}$ and winning conditions in the verification gadget
holds:

\begin{lemma}\label{lem:veri}
Let $\GG^n_{\psi}$ be the game-arena of $\psi$, and let $(E,\{s_{m+1},s_{m+1}\})$
be a configuration, where all variables are assigned in $\GG^n_{\psi}$,
the edges of the verification gadget intact, and defender is about to move.
The defender wins iff $\alpha(\GG^n_{\psi}) \models \psi$.
\end{lemma}

A run through the verification gadget starts with two agents arriving at $s_{m+1}$ and
the defender removing $(s_{m+1},f)$. The agents need to split, as the defender wins by either removing $(d_l,e_l)$ or $(d_r,f)$ and then $(e_r,f_r)$. 
After two steps, the agents will reach $f_l$ and $f_r$, defender removing $(f_r,f)$.
The left agent can now choose a clause of the 
formula, with the intention to falsify it. Assume he decides 
to move to $l_{j1}$, whereas the right agent moves to $l_{r1}$. W.l.o.g. assume
$L_{j1} = X_1$, $L_{j2} = X_2$ and $L_{j3} = X_3$. 
If $\alpha(G^n_{\psi}) \models L_{j1}$, the defender wins by Lemma~\ref{lem:veri_literals}.1 and if $\alpha(G^n_{\psi}) \not \models L_{j1}$, he removes either $(x_i,f)$ or $(l_{j1},x_i)$.
The agents move to $g_1$ and $g_l$ ($g_r$), defender removes $(g_l,f)$ ($(g_r,f)$), agents move to $l_{j2}$ and $l_{r2}$. Now, if $\alpha(G^n_{\psi}) \models L_{j2}$, we can apply 
Lemma~\ref{lem:veri_literals}.2, otherwise defender removes $(x_2,f)$ or $(l_{j2},x_2)$,
and agents move to $l_{j3}$ and either $h_l$ or $h_r$, and we can apply Lemma~\ref{lem:veri_literals}.3. Thus the ``only-if'' direction of Lemma~\ref{} holds.
For the reverse, with the above observation, clearly 
if the defender looses, then $\alpha(G^n_{\psi}) \not \models (L_{j1} \lor L_{j2} \lor L_{j3})$, and thus $\alpha(G^n_{\psi}) \not \models \psi$.

All in all, Lemma~\ref{lem:g_qbf_psi} follows from
Lemmata~\ref{lem:filtering}, \ref{lem:universal}, \ref{lem:existential}, \ref{lem:veri} 
and construction of $\GG^n_{\psi}$.


\section{Games with infinitely many agents}\label{sec:np-hard}

One might ask, what happens if there is a infinite supply of 
agents to ``flood'' a network.  Then there are always 
enough agents to move alongside any outgoing edge in any 
configuration. 

%DK changed notion of configuration according to new definition, f -> \sigma
Given an arena $(G,s,f)$, the initial configuration of a 
game with infinitely many agents
is $(E_{\text{in}},A_{\text{in}})$, where 
$A_{\text{in}}$ is a multiset containing the element $s$
with cardinality $\mathbb{N}$. Let $C$ be the set of 
configurations.
A strategy of the agents is a function $\sigma: C \to C$ with
$c \toa \sigma(c)$ for all $c \in C$. Let $(E,A) \toa (E',A')$ 
be a move of the agents with multisets $S$ and $M$ as defined.
A move is \emph{all-exploring} if 
$\{ s \mid s \in A, (s,t) \in E \} \setminus M_s = \varnothing$.
Here the set $M_s$ denotes the underlying set of elements of $M$.
A strategy $\sigma$ is \emph{all-exploring} 
if for all $c \in C$, the move $c \toa \sigma(c)$ is all-exploring.
The agents play according to a strategy $\sigma$, if whenever
being in configuration $c$, agents move $c \toa \sigma(c)$.

\begin{quote}%dk:changed name INFTY-AGENT BLOCKING
\emph{INFTY-AGENT BLOCKING} is the following decision problem: \\
\textsf{Input:} A game-arena $\GG$. \\
\textsf{Question:} Does the defender win in $\GG$ against infinitely many agents?
\end{quote}

Note that an all-exploring strategy is always optimal for the agents:

\begin{lemma}
Let $\GG$ be a game-arena. Fix any all-exploring strategy $\sigma$.
The defender wins in $\GG$ against infinitely many agent 
iff he wins against infinitely agents playing according to $\sigma$.
\end{lemma}

Thus to decide the blocking problem against infinitely many agents,
it suffices to only consider one unique move of the agents in
a configuration. However this does not shift the problem to $P$:

%DK if possible, I'd like to not define a subsection here, esp. if we later
%put large parts of the proof in the appendix
%\subsection{NP-hardness of games against infinitely many agents}

\begin{theorem}\label{thm:np-complete}
INFTY-AGENT BLOCKING is NP-complete.
\end{theorem}

Here we only show NP-hardness. For it,
we give a reduction 
from the NP-complete problem SAT~\cite{CO71}.
Let $\varphi$ be a quantifier free formula over $m$ Boolean variables 
$x_1, \ldots x_n$ in conjunctive normal form. Then 
$\psi = \exists x_1 \ldots \exists x_m \varphi$ is an instance of SAT.
Note that w.l.o.g. we can require each clause to contain exactly three variables.
Analogous to the reduction from QBF, we will construct a game-arena
$\GG_{\psi}$ polynomial in the size of the formula, where
the defender wins against infinitely many agents
iff the instance of SAT has a satisfying assignment.

\begin{lemma}\label{lem:g_sat_psi}
Let $\psi$ be an instance of SAT.
The defender wins on $\GG_{\psi}$
iff $\psi$ has a satisfying assignment.
\end{lemma}

Lemma~\ref{lem:g_sat_psi} and polynomial size of the game 
arena in the size of $\psi$, proves 
Theorem~\ref{thm:np-complete}. We 
construct existential gadgets for each variable and a verification gadget,
and first connect all existential gadget, and then the exit of the last 
existential gadget with the verification gadget.
Since the construction of $G_{\psi}$ is quite 
analogue to the construction of $G_{\psi}^n$ of the previous
section, we skip a detailed analysis of the traversal.

\begin{figure}[hbt]%
  \centering
  % The existential gadget for infintiely many attackers
  \begin{tikzpicture}[scale=0.2,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(fake_in)	at (0,0)			{};
 	\node[]								(a)			[right of=fake_in]  {$s_i$};
    \node[node distance=0.8cm]			(b)			[below of=a] {$a$};    
   
    \node[node distance=2.41cm, style=final](f) 	[below of=b]		{$\bullet$};    
    \node[node distance=2cm]			(bl)		[below left of=b]	{$b_l$};
    \node[node distance = 2cm]			(br)		[below right of=b]	{$b_r$};   

    \node[]								(cl)		[below of=bl]		{$c_l$};   
    \node[]								(cr)		[below of=br]		{$c_r$};   
    \node[]								(el)		[below of=cl]		{$x_i$};   
    \node[]								(er)		[below of=cr]		{$\neg x_i$};   
    \node[]								(dl)		[left of=el]		{$d_l$};   
    \node[]								(dr)		[right of=er]		{$d_r$};   
    \node[node distance=2cm]			(g)			[below of=f]		{$s_{i+1}$};
    \node[]								(o)			[below of=g]		{};

    
    \node[node distance=2cm]			(h)			[left of=cl]		{$h$};    
    \node[]								(i)			[below of=h]		{$i$};
    \node[style=final]					(f2)		[left of=i]			{$\bullet$};
    \node[]								(k)			[below of=i]		{$k$};
    \node[]								(j)			[below of=f2]		{$j$};

    \node[node distance=3cm]		(from_veri1)[above left of=i]	{\tiny{ver. gadget}};
    \node[node distance=1.5cm]		(from_veri2)[above right of=dr]	{\tiny{ver. gadget}};
 
	\draw[]							(b)		to node[auto]	{}	(bl); 
	\draw[]							(b)		to node[auto]	{}	(br);     
	\draw[]							(bl)	to node[auto]	{}	(cl); 	
	\draw[]							(br)	to node[auto]	{}	(cr); 		
	\draw[]							(cl)	to node[auto]	{}	(dl); 		
	\draw[]							(cr)	to node[auto]	{}	(dr); 		
	\draw[]							(dl)	to node[auto]	{}	(g); 	
	\draw[]							(dr)	to node[auto]	{}	(g); 	
	\draw[]							(dl)	to node[auto]	{}	(el); 	
	\draw[]							(dr)	to node[auto]	{}	(er); 			
		
	\draw[]							(h)		to node[auto]	{}	(i); 	
	

	\draw[]							(k)		to node[auto]	{}	(g); 	
	\draw[]							(i)		to node[auto]	{}	(k); 	
	\draw[]							(k)		to node[auto]	{}	(j); 	
	\draw[]							(j)		to node[auto]	{}	(f2); 	
	
	\draw[]							(cl)	to node[auto]	{}	(f); 	
	\draw[]							(bl)	to node[auto]	{}	(f); 	
	\draw[]							(cr)	to node[auto]	{}	(f); 	
	\draw[]							(br)	to node[auto]	{}	(f); 	
	\draw[]							(el)	to node[auto]	{}	(f); 	
	\draw[]							(er)	to node[auto]	{}	(f); 	

	

	\draw[]							(a)		to node[auto]	{}	(b);
    \draw[style=ledge,dotted]	(fake_in)	to node[auto]	{in}    (a);   
    \draw[style=ledge,dotted]	(g)			to node[auto]	{out}	(o);

	\draw[bend left=30,style=ledge,dotted]	(from_veri1) to node[auto] {} (el);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (er);
	\draw[bend right=10]		(b)	to node[auto]	{}	(h);

	
  \end{tikzpicture}
  \caption{existential gadget for  infinitely many agents.}
  \label{fig:existential-gadget-inf}
\end{figure}



%A traversal starts after agents moved to $c_1$. Either $(c_1,l_{11})$ or $(c_1,b_{11})$ has 
%to be deleted, for otherwise the agents win. Assume $l_{11} = x_i$ and $x_i$ is assigned
%to \textsc{True} in $\GG_{\psi}$. Then he deletes $(c_1,b_{11})$. Agents move to $l_{11}$ 
%and the defender deletes $(l_{11},f)$. Now agents move in parallel to $d_{11}$, back to $x_i$, and to $e_1$. Since $x_i$ is a sink state and no longer connected to $f$, the defender can delete $(d_{11},f)$, agents move to $c_2$ and the verification starts for clause $2$. If $x_i$ is 
%assigned to \textsc{false} in $\GG_{\psi}$, the defender deletes $(c_1,l_{11})$ in the first steps and after two steps and deletions, agents arrive at $b_{13}$ and an analogous situation occurs for literal $l_{12}$. The defender may choose to verify his assignment with $l_{12}$ or lead agents to $b_{15}$, when his assignment verifies $l_{13}$. After that, clause $2$ is verified and so on, until $c_k$ is verified.

\begin{figure}[hbt]%
  \centering
  % The verification gadget, infinitely many attackers
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(fake_in)	at (0,0)			{};
 	\node[]								(c1)		[below of=fake_in]  {$c_1$};
 	\node[node distance=2cm]			(c2)		[right of=c1] 		{$c_2$};
 	\node[node distance=4.5cm]			(ck)		[right of=c2]		{$c_p$};
 	
 	\node[node distance=2cm]			(fake_belowc2)[below of=c2]		{};
 	\node[node distance=4cm]			(fake_belowc21)[below of=c2]	{};
 	\node[node distance=1.5cm]			(fake_rightc2)[right of=c2]		{};
 	\node[node distance=3cm]			(fake_rightc21)[right of=c2]	{};
 	
 	\node[]								(abovec2)	[above of=c2]		{$e_1$};
 	\node[]								(aboveck)	[above of=ck]		{$e_{p-1}$};
 	
 	\node[node distance=1.8cm]			(fake_in_ck1)	[left of=aboveck] {};
 	\node[node distance=2.3cm]			(fake_in_ck2)	[left of=aboveck] {};
 	\node[node distance=2.8cm]			(fake_in_ck3)	[left of=aboveck] {};

 	\node[]								(b1)		[below of=c1]		{$b_{11}$};
 	\node[]								(l11)		[left of=b1]		{$l_{11}$};
 	\node[]								(fake_l11l)	[left of=l11]		{$d_{11}$};
 	\node[style=final]					(f1)		[left of=fake_l11l]	{$\bullet$};
	\node[]								(back11)	[below of=fake_l11l]{};
	\node[style=final]					(f2)		[right of=b1]		{$\bullet$};
	\node[]								(b2)		[below of=b1]		{$b_{12}$};
	\node[style=final]					(f3)		[right of=b2]		{$\bullet$};
	\node[]								(b3)		[below of=b2]		{$b_{13}$};
	\node[]								(b4)		[below of=b3]		{$b_{14}$};
	\node[]								(l12)		[left of=b4]	{$l_{12}$};
	\node[]								(fake_l12l)	[left of=l12]		{$d_{12}$};
	\node[style=final]					(f4)		[left of=fake_l12l]	{$\bullet$};
	\node[]								(back12)	[below of=fake_l12l]{};
	\node[style=final]					(f5)		[right of=b4]		{$\bullet$};
	\node[]								(b5)		[below of=b4]		{$b_{15}$};
	\node[style=final]					(f6)		[right of=b5]		{$\bullet$};
	\node[]								(fake_l13)	[below of=b5]		{};
	\node[]								(l13)		[left of=fake_l13]	{$l_{13}$};
	\node[]								(fake_l13l)	[left of=l13]		{$d_{13}$};			
	\node[style=final]					(f7)		[left of=fake_l13l] {$\bullet$};
	\node[]								(fake_l14)	[below of=l13]		{};
	\node[]								(back13)	[left of=fake_l14]	{};
		
	\draw[]							(c1)	to node[auto]	{}	(l11); 	
	\draw[]							(c1)	to node[auto]	{}	(b1); 	
	\draw[]							(l11)	to node[auto]	{}	(fake_l11l); 		
	\draw[]							(fake_l11l)	to node[auto]	{}	(f1); 	
	\draw[]							(b1)	to node[auto]	{}	(b2); 		
	\draw[]							(b1)	to node[auto]	{}	(f2); 		
	\draw[]							(b2)	to node[auto]	{}	(f3); 	
	\draw[]							(b2)	to node[auto]	{}	(b3); 		
	\draw[]							(b3)	to node[auto]	{}	(l12); 	
	\draw[]							(b3)	to node[auto]	{}	(b4); 		
	\draw[]							(b4)	to node[auto]	{}	(b5); 		
	\draw[]							(b4)	to node[auto]	{}	(f5); 		
	\draw[]							(b5)	to node[auto]	{}	(f6); 		
	\draw[]							(l12)	to node[auto]	{}  (fake_l12l);
	\draw[]							(fake_l12l)	to node[auto]	{}  (f4);	
	\draw[]							(b5)	to node[auto]	{}  (l13);	
	\draw[]							(l13)	to node[auto]	{}  (fake_l13l);	
	\draw[]							(fake_l13l)	to node[auto]	{}  (f7);	
	
	\draw[bend right =40]			(l11)	to node[auto]	{}  (f1);	
	\draw[bend right =40]			(l12)	to node[auto]	{}  (f4);	
	\draw[bend right =40]			(l13)	to node[auto]	{}  (f7);		
	
	\draw[style=ledge,dotted]		(l11)		to node[auto]	{\tiny{back}}	(back11);		
	\draw[style=ledge,dotted]		(l12)		to node[auto]	{\tiny{back}}	(back12);	
	\draw[style=ledge,dotted]		(l13)		to node[auto]	{\tiny{back}}	(back13);	
	

 	\node[]								(bk1)		[below of=ck]		{$b_{p1}$};
 	\node[]								(lk1)		[left of=bk1]		{$l_{p1}$};
 	\node[]								(fake_lk1l)	[left of= lk1]		{$d_{p1}$};
 	\node[style=final]					(fk1)		[left of=fake_lk1l]	{$\bullet$};
	\node[]								(backk1)	[below of=fake_lk1l]{};
	\node[style=final]					(fk2)		[right of=bk1]		{$\bullet$};
	\node[]								(bk2)		[below of=bk1]		{$b_{p2}$};
	\node[style=final]					(fk3)		[right of=bk2]		{$\bullet$};
	\node[]								(bk3)		[below of=bk2]		{$b_{p3}$};
	\node[]								(bk4)		[below of=bk3]		{$b_{p4}$};	
	\node[]								(lk2)		[left of=bk4]		{$l_{p2}$};
	\node[]								(fake_lk2l)	[left of=lk2]		{$d_{p2}$};
	\node[style=final]					(fk4)		[left of=fake_lk2l]	{$\bullet$};
	\node[]								(backk2)	[below of=fake_lk2l]{};
	\node[style=final]					(fk5)		[right of=bk4]		{$\bullet$};
	\node[]								(bk5)		[below of=bk4]		{$b_{p5}$};
	\node[style=final]					(fk6)		[right of=bk5]		{$\bullet$};
	\node[]								(fake_lk3)	[below of=bk5]		{};
	\node[]								(lk3)		[left of=fake_lk3]	{$l_{p3}$};
	\node[]								(fake_lk3l)	[left of=lk3]		{$d_{p3}$};			
	\node[style=final]					(fk7)		[left of=fake_lk3l] {$\bullet$};
	\node[]								(fake_lk4)	[below of=lk3]		{};
	\node[]								(backk3)	[left of=fake_lk4]	{};
		
	\draw[]							(ck)	to node[auto]	{}	(lk1); 	
	\draw[]							(ck)	to node[auto]	{}	(bk1); 	
	\draw[]							(lk1)	to node[auto]	{}	(fake_lk1l); 		
	\draw[]							(fake_lk1l)	to node[auto]	{}	(fk1); 	
	\draw[]							(bk1)	to node[auto]	{}	(bk2); 		
	\draw[]							(bk1)	to node[auto]	{}	(fk2); 		
	\draw[]							(bk2)	to node[auto]	{}	(fk3); 	
	\draw[]							(bk2)	to node[auto]	{}	(bk3); 		
	\draw[]							(bk3)	to node[auto]	{}	(lk2); 	
	\draw[]							(bk3)	to node[auto]	{}	(bk4); 		
	\draw[]							(bk4)	to node[auto]	{}	(bk5); 		
	\draw[]							(bk4)	to node[auto]	{}	(fk5); 		
	\draw[]							(bk5)	to node[auto]	{}	(fk6); 		
	\draw[]							(lk2)	to node[auto]	{}  (fake_lk2l);
	\draw[]							(fake_lk2l)	to node[auto]	{}  (fk4);	
	\draw[]							(bk5)	to node[auto]	{}  (lk3);	
	\draw[]							(lk3)	to node[auto]	{}  (fake_lk3l);	
	\draw[]							(fake_lk3l)	to node[auto]	{}  (fk7);	
	
	\draw[bend right =40]			(lk1)	to node[auto]	{}  (fk1);	
	\draw[bend right =40]			(lk2)	to node[auto]	{}  (fk4);	
	\draw[bend right =40]			(lk3)	to node[auto]	{}  (fk7);		
	
	\draw[style=ledge,dotted]		(lk1)		to node[auto]	{\tiny{back}}	(backk1);		
	\draw[style=ledge,dotted]		(lk2)		to node[auto]	{\tiny{back}}	(backk2);	
	\draw[style=ledge,dotted]		(lk3)		to node[auto]	{\tiny{back}}	(backk3);	

 	\draw[style=dotted] (fake_belowc2) 	to[-] node[auto] {} (fake_belowc21);
 	\draw[style=dotted] (fake_rightc2) 	to[-] node[auto] {} (fake_rightc21);

	\draw[]							(abovec2)	to node[auto]	{}	(c2);
	\draw[]							(aboveck)	to node[auto]	{}	(ck);
	
	\draw[bend left=80]		(l11)		to node[auto]		{} (abovec2);
	\draw[bend left=30]		(l12)		to node[auto]		{} (abovec2);
	\draw[bend right=40]	(l13)		to node[auto]		{} (abovec2);

	\draw[bend left=10]		(fake_in_ck1)		to node[auto]		{} (aboveck);
	\draw[bend left=20]		(fake_in_ck2)		to node[auto]		{} (aboveck);
	\draw[bend left=30]		(fake_in_ck3)		to node[auto]		{} (aboveck);

    \draw[style=ledge,dotted]	(fake_in)	to node[auto]	{in}    (c1);  

  \end{tikzpicture}
  \caption{Verification-gadget, infinitely many agents, $p$ clauses.}
  \label{fig:verification-gadget-inf}
\end{figure}

\section{Blocking problem over trees}\label{sec:tree}

Throughout this section we use the following definitions:
A tree $T$ is a directed acyclic graph such that i) there exists exactly one vertex with indegree $0$ (the root) ii) there exists one vertex with indegree $> 0$ (the goal) and iii) all other vertices have indegree $1$. The depth of a tree is the length of a maximal path, formally $\text{depth}(T) = \max \{ i \in \mathbb{N} \mid V^i \not = \varnothing \}$. where $V^i$ is the set of nodes with a path from the root of length $i$. With $E(i)$ we denote the outgoing
edges w.r.t. to $V^i$, that is $E(i) = \{ (u,v) \in E \mid u \in V^i \}$. The size of a tree $|T|$ is the number of its edges. We say $M$ is a multiset \emph{over} a set $N$ when $N$ is the underlying set of $M$. We speak of decision problems $n$/INFTY-AGENT BLOCKING \emph{over trees}, when the input-arena is restricted to a tree. To solve games on trees, we can use a straight-forward attractor construction of the winning-sets of the agents, starting with the most-distant configurations and iteratively consider previously reachable ones. Our result is that as long as we fix the number of the agents and regard it as a constant, the problem becomes polynomially
tractable for arbitrary sized trees, but remains NP-hard, if we allow infinitely many agents.

\begin{definition}
Let $\GG = (T, s, f)$ and $d = \text{depth}(T)-1$. Let $0 \leq i < d$. We define recursively the \emph{winning sets} $W_i$ of the agents:
\begin{align*}
W_d = \{ & A \mid \text{$A$ is a multiset over $V^d$, $2 \leq |A| \leq n$} \} \\
W_{i} = \{ & A \mid \text{$A$ is a multiset over $V^{i}$}, 1 \leq |A| \leq n, \text{and $f \in A$ or}   \\
&	\forall e \in E(i) \,\ \exists B \in W_{i+1}: 
	(E_{\text{in}} \setminus \{e \},A) \toa (E_{\text{in}} \setminus \{ e \},B) \}
\end{align*}
\end{definition}

\begin{lemma}\label{thm:sound_correct}
Let $\GG = (T,s,f)$ be a game-arena with root $s$ and goal $f$ and $d = \text{depth}(T)-1$. The 
defender wins on $\GG$ against $n$ agents iff $W_0 = \varnothing$.
\end{lemma}

%We skip the proof for Theorem~\ref{thm:sound_correct}, but mention that the key point is here that whenever the defender has a winning strategy, he has one where he deletes in step $i$ an edge from $\{ (v,u) \mid v \in V^i \}$. Thereby the number of all branchings that need to be considered is reduced significantly.

\begin{theorem}
Let $(T,s,f)$ be a game-arena over a tree $T$ with root $s$, where
$n$ agents placed at $s$. Then $W_0$ can be 
computed in time $O(|T|^{n})$.
\end{theorem}
\begin{proof}
We only give a brief sketch:
The size of $W_i$ can be (over)estimated in the following way:
Since the size of each multiset in $W_i$ is limited by $n$, 
and there are $|V^i|$ choices for each element, we
have $W_i \leq |V^i|^n \leq |T|^n$. We can first generate the set
of all potential elements of $W_i$, and then filter out those
that do not adhere the conditions. The first condition can
be checked during the construction, and to check the second
condition for $W_i$, we need to remove each of $|E(i)|$ edges, 
and then,
for each of this removal test all potential moves of the agents.
Each of the $n$ many agents at, say $u$, has at most 
$\textsf{outdeg}(u)$ choices to move. Thus there are
at most $|\sum_{u \in V^i} \textsf{outdeg}(u)|^n \leq |T|^n$
moves that have to be tested $|E(i)|$ times. Then one $W_i$ can
be computed in 
\[
O(|T|^n \cdot |E(i)| \cdot |T|^n) \in O(|T|^{2n+1}) \in O(|T|^n)
\] and since there are at most $\text{depth}(T) \leq |T|$ sets $W_i$
to generate, $W_0$ can be computed in $|T| \cdot O(|T|^n) \in O(|T|^n)$.
\end{proof}

\begin{corollary}
$n$-AGENT BLOCKING over trees is decidable in $O(|T|^n)$.
\end{corollary}

\noindent For infinitely man agents however, NP-hardness remains. In \cite{KG10}, the following variant of the Firefighter-problem is introduced and shown to be NP-hard:
\begin{quote}
3-FL-FIRE is the following decision problem: \\
\textsf{Input:} A full rooted~\footnote{A tree is full rooted, if all leaves have the same distance from the root} tree $T$ with maximum degree $3$ and root $r$. \\
\textsf{Question:} Is there a sequence of vertex deletions, such that no leaf burns?
\end{quote}

\noindent In 3-FL-FIRE, in the first step a fire breaks out at the root. In each subsequent
step, the firefighter defends a vertex which is not on fire (the vertex stays protected afterwards), and then, when a vertex 
is burning, the fire spreads to all children of the vertex. This continues, until
the fire cannot spread anymore.
Thus the main difference between 3-FL-FIRE and INFTY-AGENT BLOCKING over trees is merely edge-deletions vs. vertex deletions. A reduction is straight-forward, we skip the details here.

\begin{theorem}
The is a linear reduction from 3-FL-FIRE to INFTY-AGENT BLOCKING over trees.
\end{theorem}

\section{Conclusion}\label{sec:Conclusion}

We gave a thorough analysis of the complexity of reachability of multiple 
agents moving in a graph under failure, considering several scenarios.
A maybe somewhat counterintuitive result is that, the complexity does not
increase, if we do the step form finite to infinite agents.

\subsubsection*{Acknowledgements}

We thank Nao Hirokawa for his valuable comments on an earlier draft.

\bibliographystyle{lncs}
\selectlanguage{english}
\bibliography{references}

\newpage
\end{document}